Inference at * 1 
Iof proof for Lemma do-apply-p-co-filter:



1. T : Type
2. P : T
3. f : x:T. Dec(P(x))
4. x : T
  (isl(case f(x) of inl(p) => inr p  | inr(p) => inl x ))
   (outl(case f(x) of inl(p) => inr p  | inr(p) => inl x ) = x) 

latex

 by ((((GenConcl f(x) = z) 
CollapseTHENA (Auto))) 
CollapseTHEN (((D (-2)) 
CollapseTHEN (((
CoReduce 0) 
CollapseTHEN (Auto)))))) 

latex

Co.

Definitions

s = t, Dec(P), x(s), f(a), , x:AB(x), t  T, P  Q, left + right, False, b, x:A. B(x), P  Q, True